-
Notifications
You must be signed in to change notification settings - Fork 0
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
create cfa checker for unique #221
base: formal-verification
Are you sure you want to change the base?
Conversation
09ff50c
to
74cb389
Compare
358a1d5
to
5874959
Compare
5874959
to
e4fc535
Compare
Forced updated this pr with current formver branch, for now a basic structure of CFA visitor with stack for intermediate expression unique information is established. |
ef9a105
to
e4fc535
Compare
plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCFA.kt
Outdated
Show resolved
Hide resolved
|
||
interface UniqueCheckerContext { | ||
val config: PluginConfiguration | ||
val errorCollector: ErrorCollector | ||
val session: FirSession | ||
val uniqueId: ClassId | ||
val uniqueStack: ArrayDeque<ArrayDeque<PathUnique>> |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is a confusing type to work with. Could you make a dedicated class for this, please? Preferably both the stack and its elements, I suspect.
Why is it a Deque if you want to use it as a stack?
sealed class PathUnique | ||
data class Path(val symbol: FirVariableSymbol<FirVariable>) : PathUnique() | ||
data class Level(val level: Set<UniqueLevel>) : PathUnique() |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Please add some comments for these types. What do they denote?
plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCFA.kt
Outdated
Show resolved
Hide resolved
if (node is EnterNodeMarker) { | ||
context.uniqueStack.add(ArrayDeque()) | ||
} else if (node is ExitNodeMarker) { | ||
context.uniqueStack.popLast().lastOrNull()?.let { context.uniqueStack.last().add(it) } | ||
} | ||
return data |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This function seems to always be called explicitly; it's not that these nodes are handled automatically by it. Two helper function onEnter
and onExit
would probably work better.
} catch (e: Exception) { | ||
errorCollector.addErrorInfo("... while checking uniqueness level for ${declaration.source.text}") |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We use this kind of info when producing internal errors. I would actually not use ErrorCollector
here at all; you already have the reporter
.
data: PathAwareControlFlowInfo<FirVariableSymbol<FirVariable>, Set<UniqueLevel>>, | ||
): PathAwareControlFlowInfo<FirVariableSymbol<FirVariable>, Set<UniqueLevel>> { | ||
// TODO: this is where function call parameter checking should happen | ||
// Here do not call visitNode |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why not?
plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCFA.kt
Outdated
Show resolved
Hide resolved
plugins/formal-verification/formver.uniqueness/src/org/jetbrains/kotlin/formver/UniqueCFA.kt
Outdated
Show resolved
Hide resolved
val passedUnique: Set<UniqueLevel> = when (varUnique) { | ||
is Path -> data[NormalPath]?.get(varUnique.symbol) ?: setOf(UniqueLevel.Shared) | ||
is Level -> varUnique.level | ||
} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
At this point, shouldn't we be taking some kind of meet or join?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes, this is where meet should happen, let me implement a very simplified version of it
For now, it just adds an extra CFA checker to the code, while need to remove the original one and add some basic functionality with some testing